help-page
How do you use LogicBox?
Create a new proof
Create a new proof by clicking on the ➕ icon on the front page. Then enter the name of the proof, and the type of logic the proof is in.
- propositional logic: with atomic formulas
- predicate logic: with quantifiers
- arithmetic: with addition
(note: when a proof is created, it contains a single line with no formula or rule specified)
Add a line
Add a line to your proof by right-clicking on an existing step and clicking on ⬆️ to add a line above or on ⬇️ to add a line below.
Enter a formula
Modify the formula of a line by double-clicking on it, and entering the new value.
(alternatively, you can right-click and choose 'Edit')
Choose a rule
Choose a rule by clicking on the rule and selecting a new one from the side-panel. By hovering on a rule, you may see its definition.
(note: when a new line is created, "???" is displayed to indicate no rule)
Pick lines to refer to
To refer to a line, click on a reference, then click on the line/box which you would like to refer to.
Inspect errors
You may inspect the errors currently on a line/box by clicking on it, and viewing the errors in the side-panel.
If no line/box is currently selected, the errors pertaining to the currently hovered element will be shown.
Add a box
Add a box to the proof by right-clicking on an existing step and clicking on ⬆️ to add a box above or on ⬇️ to add a box below.
Remove a step
You may remove a line by right-clicking on it and selecting 'Delete'.
If you remove a box, you will remove all steps it contains.
Move a step
You can move a line/box by dragging it to its new location
Edit fresh variable in a box (only in predicate logic/arithmetic)
You may add/edit a fresh variable by right-clicking on a box and choosing 'Edit fresh variable'.
Alternatively you may double-click on the box to edit its fresh variable
Syntax
Propositional logic
| Syntax | ||
|---|---|---|
| Propositional atoms | a, b, p, q, ... |
|
| Conjunction (and) | p and q, p A q, p ∧ q |
|
| Disjunction (or) | a or b, a V b |
|
| Implication (if ... then) | q implies r, q -> r, q => r |
|
| Negation (not) | not s, !s, ¬s |
|
| Contradiction | false, bot |
|
| Tautology | true, top, |
The following precedence rules apply (Huth, Micheal 1962, convention 1.3, page 5)
- then
- then
As examples, this means that
not p and qis parsed asp and q or ris parsed asp -> q -> ris parsed as
Note: if an ambiguous formula (such as p and q and r) is entered, it will automatically be converted to an unambiguous form (in this case
Predicate logic
| Syntax | ||
|---|---|---|
| Universal quantification (for all) | forall x P(x), ∀x P(x) |
|
| Existensial quantification (exists) | exists y Q(y), ∃y Q(y) |
|
| Predicate | P(a, b, c) |
|
| Equality | x = y |
|
| Variables | x, y, z, x_0, k_{123} |
|
| Function application | f(x, y, z) |
The symbols
The following precedence rules apply (Huth, Micheal 1962, convention 2.4, page 101)
- then
- then
As examples, this means that
forall x P(x) and not Q(x)is parsed asP(a) and Q(b) or R(c)is parsed asP(a) -> Q(b) -> R(c)is parsed as
Note: nullary predicates are also supported. As an example, this means that that the formula forall x S -> Q(x) (
Arithmetic
| Syntax | ||
|---|---|---|
| Universal quantification (for all) | forall x P(x), ∀x P(x) |
|
| Existensial quantification (exists) | exists y Q(y), ∃y Q(y) |
|
| Equality | x = y |
|
| Variables | x, y, z, x_0, k_{123} |
|
| Addition (plus) | x + y |
|
| Multiplication (times) | x * y |
|
| Zero, One | 0, 1 |
As arithmetic is just an instance of predicate logic with no predicate symbols, the constants (or nullary functions)